pre-init1-p(es;i;x;X;x0;a;p;P)
== (((P(x0)))  (e:E. (loc(e) = i)))
== & ((vartype(i;x) r X)
== & (c (e@i. (kind(e) = locl(a))  ((valtype(e) r Outcome) c ((P(x when e))))
== & (c & e@i. e'e.(kind(e') = locl(a))  (((P((x after e')))))))
== & @i x initially x0:X 

latex

---

clarification:

pre-init1-p(es;i;x;X;x0;a;p;P)
== (((P(x0)))  (e:es-E(es). (es-loc(es; e) = i  Id)))
== & ((es-vartype(es; i; x) r X)
== & (c (alle-at(es;i;e.(es-kind(es; e) = locl(a)  Knd)
== & (c  ((es-valtype(es; e) r p-outcome(p)) c ((P(es-when(es; x; e))))))
== & (c & alle-at(es;i;e.existse-ge(es;e;e'.(es-kind(es; e') = locl(a)  Knd)
== & (c &  (((P(es-after(es; x; e')))))))))
== & init-p(es; i; X; x; x0) 

latex

Definitions	x:A. B(x), E, Id, loc(e), vartype(i;x), P & Q, P  Q, A c B, valtype(e), Outcome, x when e, e@i. P(e), e'e.P(e'), P  Q, s = t, Knd, kind(e), locl(a), A, b, f(a), (x after e), @i x initially v:T
FDL editor aliases	pre-init1-p